Nuprl Definition : ma-join
0,22
postcript
pdf
M1
M2
== mk-ma(1of(
M1
)
1of(
M2
);
==
1of(2of(
M1
))
1of(2of(
M2
));
==
1of(2of(2of(
M1
)))
1of(2of(2of(
M2
)));
==
1of(2of(2of(2of(
M1
))))
1of(2of(2of(2of(
M2
))));
==
1of(2of(2of(2of(2of(
M1
)))))
1of(2of(2of(2of(2of(
M2
)))));
==
1of(2of(2of(2of(2of(2of(
M1
))))))
1of(2of(2of(2of(2of(2of(
M2
))))));
==
1of(2of(2of(2of(2of(2of(2of(
M1
)))))))
1of(2of(2of(2of(2of(2of(2of(
M2
)))))));
==
1of(2of(2of(2of(2of(2of(2of(2of(
M1
))))))))
1of(2of(2of(2of(2of(2of(2of(2of(
M2
))))))));
==
1of(2of(2of(2of(2of(2of(2of(2of(2of(
M1
)))))))))
==
1of(2of(2of(2of(2of(2of(2of(2of(2of(
M2
)))))))));
==
1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
M1
))))))))))
==
1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
M2
))))))))));
==
1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
M1
)))))))))))
==
1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
M2
))))))))))))
latex
clarification:
M1
M2
== mk-ma(fpf-join(IdDeq;1of(
M1
);1of(
M2
));
==
fpf-join(KindDeq;1of(2of(
M1
));1of(2of(
M2
)));
==
fpf-join(IdDeq;1of(2of(2of(
M1
)));1of(2of(2of(
M2
))));
==
fpf-join(IdDeq;1of(2of(2of(2of(
M1
))));1of(2of(2of(2of(
M2
)))));
==
fpf-join(product-deq(Knd;Id;KindDeq;IdDeq);1of(2of(2of(2of(2of(
M1
)))));1of(2of(2of(2of(2of(
== fpf-join(product-deq(Knd;Id;KindDeq;IdDeq);1of(2of(2of(2of(2of(
M1
)))));1of(
M2
))))));
==
fpf-join(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);1of(2of(2of(2of(2of(2of(
== fpf-join(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);1of(
M1
))))));1of(2of(2of(2of(2of(2of(
M2
)))))));
==
fpf-join(IdDeq;1of(2of(2of(2of(2of(2of(2of(
M1
)))))));1of(2of(2of(2of(2of(2of(2of(
M2
))))))));
==
fpf-join(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);1of(2of(2of(2of(2of(2of(2of(2of(
== fpf-join(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);1of(
M1
))))))));1of(2of(2of(2of(2of(2of(2of(2of(
== fpf-join(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);1of(
M1
))))))));1of(
M2
)))))))));
==
fpf-join(KindDeq;1of(2of(2of(2of(2of(2of(2of(2of(2of(
== fpf-join(KindDeq;1of(
M1
)))))))));1of(2of(2of(2of(2of(2of(2of(2of(2of(
M2
))))))))));
==
fpf-join(KindDeq;1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
== fpf-join(KindDeq;1of(
M1
))))))))));1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
M2
)))))))))));
==
fpf-join(IdDeq;1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
== fpf-join(IdDeq;1of(
M1
)))))))))));1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
== fpf-join(IdDeq;1of(
M1
)))))))))));1of(
M2
)))))))))))))
latex
Definitions
mk-ma
,
Knd
,
product-deq(
A
;
B
;
a
;
b
)
,
IdLnk
,
Id
,
IdLnkDeq
,
KindDeq
,
f
g
,
IdDeq
,
1of(
t
)
,
2of(
t
)
FDL editor aliases
ma-join
origin